Nuprl Lemma : detach_fun_properties
13,42
postcript
pdf
T
:Type,
A
:(
T
),
d
:detach_fun(
T
;
A
). {
x
:
T
. (
(
A
(
x
)))
(
(
d
(
x
)))}
latex
Up
gen
algebra
1
Definitions of Statement
detach_fun(
T
;
A
)
Definitions
t
T
,
{
T
}
,
,
x
:
A
.
B
(
x
)
,
True
,
P
Q
,
P
&
Q
,
x
.
t
(
x
)
,
P
Q
,
T
,
P
Q
,
detach_fun(
T
;
A
)
,
x
(
s
)
,
SqStable(
P
)
Lemmas
detach
fun
wf
,
sq
stable
squash
,
decidable
assert
,
sq
stable
from
decidable
,
sq
stable
implies
,
rev
implies
wf
,
sq
stable
and
,
assert
wf
,
squash
wf
,
iff
wf
,
sq
stable
all
origin